STANFORD ARTIFICIAL INTELLIGENCE PROJECT               SEPTEMBER 1973
OPERATING NOTE 73





                      PRELIMINARY USER'S MANUAL
                                 FOR
                                 AN
                     INTERACTIVE THEOREM PROVER

                                 BY

                             JOHN ALLEN

ABSTRACT:

This document represents a  short guide to using the  theorem prover.

An earlier version of this program is described in Allen  and Luckham

[MI5].   Many  of  the  later sections  of  this  manual,  on pattern

matching  and subroutining  especially,  are still  in  a rudimentary

stage of development. Experiments demonstrating  various applications

of the strategies and the  user oriented features are described  in a

forthcoming report, "Applications of First Order Proof Procedures" by

Allen, Luckham, and Morales.











This work  was supported  in part by  the Advanced  Research Projects
Agency of the Office of  the Secretary of Defense under  Contract No.
DAHC15-73-C-0435.